Artifact for "Partial Order Reduction for Reachability Games"

An updated artifact for the paper "Partial Order Reduction for Reachability Games", accepted at CONCUR'19 with the corrections, models and modifications added for the later LMCS journal version. The source-code for the engine is found in the "verifypn-games.zip" file while the experiments and scripts to execute those are found in "reproducability.zip". Code The implementation reuses the general framework of partial order reduction applied in https://doi.org/10.1016/j.jlamp.2018.09.002 The core reduction algorithm is implemented in a (semantically equivalent and) efficient manner in PetriEngine/ReducingSuccessorGenerator.cpp Here the "prepare"-method implements the equivalent of the "St"-function of the paper (Algorithm 2), the "closure"-method implements the "Saturate"-function (Algorithm 3) and computeFinite, computeSCC, computeStaticCycles being responsible for the cycle-detection (Algorithm 1). Repeatability The repeatability-package is only available on Linux. To run the experiments as per the paper, run: ./run_POR.sh games-258 ; ./run_NPOR.sh games-258 Outputs will be generated in the "outputs" folder, and a Tex-table can be outputted by ./extract.sh games-258 Notice that we have pre-populated the outputs-folder with the results reported in the paper. The execution-scripts will NOT overwrite existing output files, and thus the outputs folder should be purged prior to a re-run of the experiments. To use a different executor (for instance sbatch on a slurm-enabled cluster for concurrent execution of the experiments), the run-commands can be prefixed as such: EXECUTOR=sbatch ./run_POR.sh games-258 The included binary is revision 258 of https://code.launchpad.net/~verifypn-cpn/verifypn/verifypn-games To limit the memory-consumption of each experiment, modify "run.sh" and change the "ulimit" memory-bound to the desired value. A "timeout"-command can also be added here to introduce a time-limit of the execution (we utilize slurm for this purpose). Notice that we measure and report the computation time excluding parsing; i.e. we report the fix-point computation-time as computed by the engine directly. Changes Since the conference version (https://doi.org/10.5281/zenodo.3252104), the following changes have been made. Models: - FMS-{D,C,N} have been added - Unneeded files have been removed Data Collection - Fixed collection of measures Engine (r.258, originally r.247): - Fixed output of measures to correspond with normal interpretation (Stored markings are now reported and collected) - Fixed wrong assignment in dependency-graph - Added patch for theoretical issue with POR-reductio